home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / ada / anna.txt < prev    next >
Text File  |  1993-07-14  |  10KB  |  266 lines
  1. This document introduces the language and the current tool status and
  2. availability.  If you have any further questions, please don't
  3. hesitate to contact us at the addresses given in the "Support" section
  4. of this document.
  5.  
  6.  
  7.                Information on Anna and the Anna Tools
  8.                --------------------------------------
  9.  
  10. Introduction
  11. ------------
  12.  
  13. Anna is a language extension of Ada to include facilities for formally
  14. specifying the intended behavior of Ada programs.  It is designed to
  15. meet a perceived need to augment Ada with precise machine-processable
  16. annotations so that well-established formal methods of specification
  17. and documentation can be applied to Ada programs.
  18.  
  19.  
  20. Language
  21. --------
  22.  
  23. The Anna language is described in many documents.  There are two
  24. readily available sources of information on the language.  One is the
  25. Springer-Verlag Anna Reference Manual, volume 260 of the Lecture Notes
  26. in Computer Science series.  The primary author is David C. Luckham.
  27. This manual may be purchased at any computer bookstore, and is
  28. probably available in any mathematical reference library.
  29.  
  30. An introductory text on using Anna is available, published by Springer
  31. Verlag in their _Silver series_, Texts and Monographs in Computer
  32. Science.  The title of this book is _Programming with Specifications:
  33. An Introduction to ANNA, A Language for Specifying Ada Programs_, by
  34. David C. Luckham.
  35.  
  36. Various aspects of the Anna language and Anna tools have been
  37. documented in technical reports and published papers.  See the
  38. bibliography for a complete list of applicable documents.
  39.  
  40.  
  41. Anna Tools
  42. ----------
  43.  
  44. The Program and Analysis Group at Stanford University has developed a
  45. prototype environment supporting the Anna language.  The first release
  46. of this environment, Anna-I, is available to anyone who wishes to
  47. experiment with it.  The tools implement a large subset of the Ada and
  48. Anna languages.  These tools include:
  49.  
  50.     -- Intermediate Representation Toolkit (Extended DIANA Formal
  51.            Interface and Implementation packages (AST), Ada/Anna
  52.            Parser, Ada/Anna Pretty Printer, AST Disk <==> Memory
  53.            package)
  54.     -- Ada/Anna Static-Semantic Rules Checker
  55.     -- Annotation Transformer
  56.     -- Portable Ada/Anna Testing and Debugging System
  57.     -- Ada/Anna AST Browser
  58.     -- Ada Logic Reasoning System (a PROLOG interface)
  59.     -- Anna Package Specification Analyzer
  60.     -- Anna Interactive Tutorial System
  61.  
  62. The Anna-I tools are completely implemented in Ada, though a small
  63. amount of X-Windows and Verdix VADS dependency exist in some of the
  64. user-interfaces.
  65.  
  66. The AST IR interface defines the common internal representation used
  67. by all the Anna-I tools---routines are exported that allow traversal
  68. and data manipulation of an AST.  The Parser parses Anna text files
  69. into the AST representation.  The Pretty Printer generates ASCII text
  70. given an AST.  The AST Disk <==> Memory package performs AST
  71. disk-to-memory conversions, and vice versa.
  72.  
  73. The Semantic Checker checks the static-semantics of the Ada and Anna
  74. code in the AST: it works in both batch and incremental modes.
  75.  
  76. The Annotation Transformer maps an Anna program to an equivalent Ada
  77. program.  That is, the Transformer replaces Anna constructs with Ada
  78. checking constructs in order to build a self-checking program.  The
  79. Testing and Debugging system can then be used to monitor the run-time
  80. behavior of the transformed program.  Currently, the Testing and
  81. Debugging system is provided with a small, command-line interface, and
  82. for some releases, an X-Windows and Emacs editor interface.
  83.  
  84. The AST Browser is an X-Windows based tool for graphically traversing
  85. and examining an Anna AST.
  86.  
  87. The Ada Logic system is an Ada package which is an interface to a
  88. Prolog interpreter.  It allows the user to build clauses and databases
  89. of knowledge, and make queries with respect to the databases.
  90.  
  91. The Specification Analyzer is an interactive tool for examining and
  92. debugging the visible part of an Ada/Anna package specification using
  93. deduction and symbolic execution.
  94.  
  95. The Anna Interactive Teaching Tutorial is an interactive tutorial for
  96. Anna.  It is designed to familiarize the user with basic Anna concepts
  97. and language facilities.  Several ``hands-on'' exercises are included.
  98. Anna Teach automatically invokes other Anna tools and the Ada compiler
  99. to check the correctness of exercises entered by the user.
  100.  
  101. We are currently developing other Anna-I tools that include:
  102.  
  103.     -- Parallel Testing and Debugging System (for Sequent
  104.            Symmetry) 
  105.     -- more robust incremental semantics capabilities for Ada and Anna 
  106.  
  107.  
  108. FTP Availability
  109. ----------------
  110.  
  111. Anonymous FTP for the Anna-I environment and various Anna papers are
  112. available on the Internet host ``anna.stanford.edu'' [36.14.0.13].
  113. The file ``pub/anna/read.me'' in this FTP account has more details;
  114. please read this document before transferring any other files.
  115.  
  116. Also, if you do acquire the Anna tools via FTP, please let us know; we
  117. like to keep track of who is using the tools, and how.
  118.  
  119.  
  120. Acquiring the Anna-I Tools
  121. --------------------------
  122.  
  123. If the FTP acquisition method is not a viable option, you may obtain
  124. an Anna-I release through postal mail.
  125.  
  126. The Anna-I release requires two 9-track, 6250-bpi magnetic tapes (one
  127. for the Anna-I tools and one for the X-Windows interface used by the
  128. Anna-I tools).  It includes the ``Anna-I Installation Guide and User's
  129. Manual.''  To obtain an Anna-I release, please send us tapes and a
  130. self-addressed, stamped, return package with applicable postage to:
  131.  
  132.     Stanford Anna Team 
  133.     Computer Systems Lab, ERL 456 
  134.     Stanford University 
  135.     Stanford, CA  94305
  136.  
  137. NOTE: Include enough postage to cover the cost of sending the magnetic
  138. tape(s) plus a 75 page document.
  139.  
  140. Most of the Anna tools rely on the use of the Verdix VADS compiler.
  141. We do not have source code for any other compiler.  However, we are
  142. available to answer any questions you might have about porting the
  143. Anna-I toolset.
  144.  
  145. If you would like a pre-compiled release of the Anna-I tools, we have
  146. releases available for the following systems:
  147.     -- Sun/4 UNIX version 4.1.2, SunAda 1.1 Ada compiler
  148.     -- Sequent Symmetry DYNIX (i386), SLI/Verdix VADS 5.5.2 Ada
  149.            compiler 
  150.  
  151. Due to the considerable time and resources required to produce a
  152. pre-compiled Anna-I release, as well as the limited hardware we have,
  153. we are only currently able to produce pre-compiled releases in these
  154. two formats.  We do not have a VAX/VMS system so we cannot provide any
  155. VAX/VMS tape format pre-compiled release of the Anna-I tools.
  156.  
  157.  
  158. Support
  159. -------
  160.  
  161. Support for learning Anna and the tool set is very limited.  A short
  162. one-day tutorial course will soon be available at a fee.  Contact us
  163. for details regarding Anna language and tools support.
  164.  
  165. An Anna User's Group is now being supported through Internet
  166. electronic mail.  Announcements of new releases, new tools, bug fixes,
  167. etc. will be posted through this medium.  To obtain information about
  168. being added to the list, please contact us as the following address,
  169. phone, or electronic mail:
  170.  
  171.     Stanford Anna Team 
  172.     Computer Systems Lab, ERL 456 
  173.     Stanford University 
  174.     Stanford, CA  94305
  175.  
  176.     (415) 723-1175 (voice) 
  177.     (415) 725-7398 (fax) 
  178.     anna-request@anna.stanford.edu
  179.  
  180.  
  181. Bibliography
  182. ------------
  183.  
  184. _Reference Manual for the Ada Programming Language_.
  185. U. S. Department of Defense, U. S. Government Printing Office,
  186.   ANSI/MIL-STD-1815A edition, January 1983.
  187.  
  188. Douglas L. Bryan and Geoffrey O. Mendal.
  189. _Exploring Ada, Volume 1_.
  190. Prentice-Hall, Englewood Cliffs, New Jersey, 1989.
  191.  
  192. G. Goos, W. A. Wulf, A. Evans Jr., and K. J. Butler.
  193. _DIANA, An Intermediate Language for Ada_.
  194. Volume 161 of _Lecture Notes in Computer Science_,
  195.   Springer-Verlag, 1983.
  196.  
  197. D.C. Luckham, Randall Neff, and David Rosenblum.
  198. _An Environment for Ada Software Development Based on Formal
  199.   Specification_.
  200. Technical Report CSL-TR-86-305, Stanford University, August 1986.
  201. Also published as an article in Ada Letters, VII(3):94--106,
  202.   May/June 1987.
  203.  
  204. David Luckham, Sriram Sankar, and Shuzo Takahashi.
  205. _Two Dimensional Pinpointing: An Application of Formal
  206.   Specification to Debugging Packages_.
  207. Technical Report CSL-TR-89-379, Stanford University, April 1989.
  208. Also published as an article in IEEE Software, 8(1):74--84,
  209.   January 1991.
  210.  
  211. David C. Luckham.
  212. _Programming with Specifications: An Introduction to ANNA,
  213.   A Language for Specifying Ada Programs_.
  214. _Texts and Monographs in Computer Science_, Springer-Verlag,
  215.   October 1990, 412 pages.
  216.  
  217. David C. Luckham, Friedrich W. von Henke, Bernd Krieg-Brueckner, and Olaf
  218.   Owe.
  219. _ANNA, A Language for Annotating Ada Programs_.
  220. Volume 260 of _Lecture Notes in Computer Science_, Springer-Verlag,
  221.   1987.
  222.  
  223. Geoffrey O. Mendal.
  224. Designing for Ada reuse: A case study.
  225. In _IEEE Computer Society Second International Conference on Ada
  226.   Applications and Environments_, pages 33--42, IEEE Computer Society, Miami
  227.   Beach, Florida, 8-10 April 1986.
  228. Also published as a Stanford University Technical Report, June 1986,
  229.   CSL-86-299.
  230.  
  231. Geoffrey O. Mendal et al.
  232. _The Anna-I User's Guide and Installation Manual_.
  233. Stanford University, Computer Systems Lab, ERL 456, Stanford, California,
  234.   version 1.5 edition, December 1992.
  235.  
  236. Randall Neff.
  237. _Ada/Anna Specification Analysis_.
  238. PhD thesis, Stanford University, Stanford, California, December 1989.
  239. Also published as a Stanford University technical report, CSL-TR-89-406.
  240.  
  241. David S. Rosenblum.
  242. _A Methodology for the Design of Ada Transformation Tools in a
  243.   DIANA Environment_.
  244. Technical Report 85-269, Stanford University, February 1985.
  245. Also published in IEEE Software, 2(2):24--33, March 1985.
  246.  
  247. David Rosenblum, Sriram Sankar, and David C. Luckham.
  248. _Concurrent Runtime Checking of Annotated Ada Programs_.
  249. Technical Report CSL-TR-86-312, Stanford University, November 1986.
  250. Also published in the _Proceedings of the 6th Conference on
  251.   Foundations of Software Technology and Theoretical Computer
  252.   Science_, Volume 241 of _Lecture Notes in Computer Science_,
  253.   Springer-Verlag, 1986.
  254.  
  255. Sriram Sankar.
  256. _Automatic Runtime Consistency Checking and Debugging of Formally
  257.   Specified Programs_.
  258. PhD thesis, Stanford University, Stanford, California, July 1989.
  259. Also published as a Stanford University Technical Report, August 1989,
  260.   CSL-TR-89-391.
  261.  
  262. Sriram Sankar and David Rosenblum.
  263. _The Complete Transformation Methodology for Sequential Runtime
  264.   Checking of An Anna Subset_.
  265. Technical Report CSL-86-301, Stanford University, June 1986.
  266.